#include "PDTCheckSpec.h"

PDTCheckSpec :: PDTCheckSpec(PDTCodeGraph & aCG, 
            PDTFunctionDec *afunc,
            PDTBehaviors *abehaviors,
            PDTPreCondition *apre,
            PDTPostCondition *apost):
    PDTEvalTraversal(aCG),
    func(afunc), behaviors(abehaviors),
    pre(apre), post(apost)
{
}

PDTCheckSpec :: PDTCheckSpec(PDTCodeGraph & aCG, 
        const string & funcName, 
        const string & specName) : PDTEvalTraversal(aCG)
{
    func = getCodeGraph().findFunction(funcName);
    if (func == NULL) {
        pdt_throw PDTFunctionNotFoundEx;
    }

    behaviors = func->findBehaviors(specName);
    if (behaviors == NULL){
        pdt_throw PDTBehaviorsNotFoundEx;
    }

    pre = func->findPre(getSpecName());
    post = func->findPost(getSpecName());
}

bool PDTCheckSpec :: buildRanges() {
    return true;
}

Traversal::RetType PDTCheckSpec :: applyInput(PDTBehavior * beh) {
    unsigned int i = 0;
    for (; i < beh->getNumInputAssignments(); i++) {
        PDTStatement * assign = beh->getInputAssignment(i);
        if (assign->traverseEx(*this) == Traversal::Stop) {
            return Traversal::Stop;
        }
    }
    return Traversal::Continue;
}

Traversal::RetType PDTCheckSpec :: applyOutput(PDTBehavior * beh) {
    unsigned int i = 0;
    for (; i < beh->getNumOutputAssignments(); i++) {
        PDTStatement * assign = beh->getOutputAssignment(i);
        if (assign->traverseEx(*this) == Traversal::Stop) {
            return Traversal::Stop;
        }
    }
    return Traversal::Continue;
}

bool PDTCheckSpec :: checkPrePostPrint(PDTBehavior * beh) 
{
    Result rc = checkPrePost(beh);
    if (rc.success) {
        string str = recommendationString(rc);
        cout << str << endl;
        return true;
    }
    return false;
}

PDTCheckSpec::Result PDTCheckSpec::checkPrePost(PDTBehavior * beh) 
{
    clearVariableValues();
    if (applyInput(beh) ==  Traversal::Stop)
        return Result().failed();
    if (pre->traverseEx(*this) == Traversal::Stop)
        return Result().failed();
    PDTConst * pConst = getValue(pre);
    bool pOfI = pConst->getBoolean();

    if (applyOutput(beh) ==  Traversal::Stop)
        return Result().failed();
    if (post->traverseEx(*this) == Traversal::Stop)
        return Result().failed();
    PDTConst * qConst = getValue(post);
    bool qOfIO = qConst->getBoolean();

    return Result( beh, false, pOfI,qOfIO);
}

bool PDTCheckSpec::clearVariableValues() 
{
    for (unsigned int i = 0; 
            i < getCodeGraph().variables.size();
            i++) {
        setValue(*getCodeGraph().variables[i], NULL);
    }
    return true;
}

bool PDTCheckSpec::getOutVariableValues(PDTBehavior * beh, VarToValMap & outValues){
    vector <PDTVar *> outVars;
    beh->getOutputVariables(outVars);
    for (unsigned int i = 0; i <outVars.size(); i++) {
        PDTVar * var = outVars[i];
        PDTNode * node = var->getNode();
        PDTConst * val = getValue(node);
        outValues[var] = val;
    }
    return true;
}

bool 
PDTCheckSpec::locateCodeBetweenPreAndPost(
    PDTListOfStatements * & list, unsigned int & idx) {
    assert(pre!=NULL);
    assert(post!=NULL);
    assert(behaviors!=NULL);

    vector<PDTNode * > & preParents = pre->getParents();

    unsigned int i = 0;
    PDTNode * node = NULL;
    for (;i < preParents.size(); i++) {
        node = preParents[i];
        if (node->isListOfStatements()) {
            break;
        }
    }
    assert (node != NULL);
#ifdef PARANOID_CHECKS
    vector<PDTNode * > & postParents = pre->getParents();
    vector<PDTNode * > & behParents = behaviors->getParents();
    i = 0;
    for (;i < postParents.size(); i++) {
        if (postParents[i]->isListOfStatements()) {
            assert(node == postParents[i]);
            break;
        }
    }
    i = 0;
    for (;i < behParents.size(); i++) {
        if (behParents[i]->isListOfStatements()) {
            assert(node == behParents[i]);
            break;
        }
    }
#endif

    list = dynamic_cast<PDTListOfStatements*>(node);

    vector<PDTNode * > &listChildren = list->getChildren();
    bool metPre = false;
    bool hasCode = false;
    node = NULL;
    i = 0;
    for (; i < listChildren.size(); i++) {
        node = listChildren[i];
        if (node == pre ) {
            metPre = true;
            continue;
        }
        if (!metPre) {
            //paranoid checks!
            assert (node != post);
            assert (node != behaviors);
            continue;
        }
        if (node == post) {
            break;
        }
        if (node == behaviors) {
            break;
        }
        hasCode = true;
        idx = i;
        break;
    }
    return hasCode;
}

Traversal::RetType PDTCheckSpec::execCodeBetweenPreAndPost(
        PDTListOfStatements & list, unsigned int idx) {
    vector<PDTNode * > &listChildren = list.getChildren();
    unsigned int i = idx;
    PDTNode * node = NULL;
    for (; i < listChildren.size(); i++) {
        node = listChildren[i];
        if (node == post) {
            break;
        }
        Traversal::RetType rc = Traversal::Skip;
        try{
            rc = node->traverseEx(*this);
            if (rc == Traversal::Stop)
                return Traversal::Stop;
        } catch(PDTCheckSpecException & e) {
            if (e == PDTReturnStatementEx) {
                break; //rc = Traversal::Continue;
            } else  {
                pdt_throw e;
            }
        }
    }
    //assert(node == post); -- not true if a return statement was met.
    return Traversal::Continue;
}

bool PDTCheckSpec::checkPreCodePostPrint(PDTBehavior * beh, 
            PDTListOfStatements & list, unsigned int idx) 
{
    Result rc = checkPreCodePost(beh, list, idx);
    if (rc.success ) {
        string str = recommendationString(rc);
        cout << str << endl;
        return true;
    }
    return false;
}

PDTCheckSpec::Result    
PDTCheckSpec::checkPreCodePost(PDTBehavior * beh, 
            PDTListOfStatements & list, unsigned int idx) 
{
    clearVariableValues();
    if (applyInput(beh) ==  Traversal::Stop)
        return Result().failed();
    if (pre->traverseEx(*this) == Traversal::Stop)
        return Result().failed();
    PDTConst * pConst = getValue(pre);
    bool pOfI = pConst->getBoolean();

    if (applyOutput(beh) ==  Traversal::Stop)
        return Result().failed();
    if (post->traverseEx(*this) == Traversal::Stop)
        return Result().failed();
    PDTConst * qConst = getValue(post);
    bool qOfIO = qConst->getBoolean();

    VarToValMap oValues;
    getOutVariableValues(beh, oValues);

    clearVariableValues();
    if (applyInput(beh) ==  Traversal::Stop)
        return Result().failed();
    //TODO: just the list of statements 
    //      starting just after pre
    //      and going until post
#if 0
    if (func->traverseEx(*this) == Traversal::Stop)
        return Result().failed();
#else
    Traversal::RetType rc = execCodeBetweenPreAndPost(list,idx);
    if (rc == Traversal::Stop)
        return Result().failed();
#endif

    VarToValMap oPrimeValues;
    getOutVariableValues(beh, oPrimeValues);

    if (post->traverseEx(*this) == Traversal::Stop)
        return Result().failed();
    PDTConst * qPrimeConst = getValue(post);
    bool qOfIOPrime = qPrimeConst->getBoolean();

    bool oEqOPrime = isEqual(oValues,oPrimeValues);

    return Result(beh, true, pOfI,qOfIO,qOfIOPrime,oEqOPrime);
}

    bool PDTCheckSpec :: isEqual(VarToValMap& lhs, VarToValMap& rhs){
        if (rhs.size() != lhs.size() )
            return false;
        VarToValMap::iterator it = lhs.begin();
        for(; it != lhs.end(); it++) {
            PDTVar * v = it->first;
            VarToValMap::iterator it2 = rhs.find(v);
            if (it2 == rhs.end())
                return false;
            PDTConst * val1 = it->second;
            PDTConst * val2 = it2->second;
            if (val1 == val2 )
                continue;
            if ( !val1->isEqual(*val2)){
                return false;
            }
        }
        return true;
    }

bool PDTCheckSpec :: checkPrePost() {
    cout << "checking {P}-{Q}{B} for spec '" << getSpecName() << "' in function '" << getFuncName() << "'." << endl;
    if (pre == NULL) {
        elog() << "No precondition. Assume P is true!" << endl;
        if (post == NULL) {
            elog() << "No postcondition. Assume Q is true! Trivial {P}-{Q}{B} check." << endl;
            return true;
        }
    }
    if (post == NULL) {
        elog() << "No precondition. Assume Q is true!" << endl;
    }
    unsigned int i = 0;
    for (; i < behaviors->getNumBehaviors(); i++ ) {
        PDTBehavior * beh = behaviors->getBehavior(i);
        stringstream ss(stringstream::in | stringstream::out);
        cout << "checking " << beh->toString(ss).str() << endl;
        checkPrePost(beh);
    }

    return true;
}

bool PDTCheckSpec :: checkPreCodePost(PDTListOfStatements & list, unsigned int  idx) {
    cout << "checking {P}S{Q}{B} for spec " << getSpecName() << " in function " << getFuncName() << "." << endl;
    unsigned int i = 0;
    for (; i < behaviors->getNumBehaviors(); i++ ) {
        PDTBehavior * beh = behaviors->getBehavior(i);

        cout << "checking ";
        stringstream ss(stringstream::in | stringstream::out);
        cout << beh->toString(ss).str() << endl;
        checkPreCodePost(beh, list, idx);
    }
    return true;
}

void
PDTCheckSpec :: check() {
    PDTListOfStatements * list = NULL;
    unsigned int idx = 0;
    bool hasCode = locateCodeBetweenPreAndPost(list, idx);
    if (hasCode) {
        checkPreCodePost(*list, idx);
    } else {
        checkPrePost();
    }
}

string
PDTCheckSpec :: Result :: advice () 
{
    stringstream ss(stringstream::in | stringstream::out);


    if (withCode) {
        if (beh->isGood()) {//good behaviors with code
            if (!PofI) {
                ss<<"Properties are not mature enough to test with code.";
                return ss.str();
            }
            bool oInGofI = oEqOPrime;
            //TODO: if !oEqOPrime then prompt the user
            //      whether oPrime is in g(i)
            bool oInQofI = QofOPrime;
        //    ss << "Required: o in g(i) and Q(i,o)" <<endl;
            if (oInGofI && oInQofI) {
                ss << " No correction needed.";
            }  else if (oInGofI && !oInQofI) {
                ss << "Weaken Q so that Q(i,o) = true.";
            } else if (!oInGofI && oInQofI) {
                ss << "Strengthen Q so that Q(i,o) = true, and " << endl;
                ss << "strengthen S so that its output is in g(i).";
            } else {
                ss << "Strengthen S so that its output is in g(i).";
            }
        } else {// bad behaviors with code
            if (oEqOPrime) {
                if (QofOPrime) {
                    ss<<" Strengthen Q so that Q(i,o) = false, and modify S so that o is not in S(i)"<<endl;
                } else {
                    ss<<"Modify S so that o is not in S(i)."<<endl;
                }
            } else {
                //TODO:
            }
        }
    }else {
        if (beh->isGood() ) {
            if (PofI && QofO) {
                ss<<"    1. Strengthen P so that P(I) = false."<<endl;
                ss<<"or  2. Skip.";
            } else if (PofI && !QofO) {
                ss<<"    1. Strengthen P so that P(I) = false."<<endl;
                ss<<"xor 2. Weaken Q so that Q(I,O) = true.";
            } else if (!PofI && QofO) {
                ss<<"    1. Weaken P so that P(I) = true."<<endl;
                ss<<"xor 2. Strengthen Q so that Q(I,O) = false."<<endl;
                ss<<"xor 3. Skip.";
            } else if (!PofI && !QofO) {
                ss<<"    1. Weaken P so that P(I) = true, and strengthen Q so that Q(I,O) = false."<<endl;
                ss<<"xor 2. Skip.";
            }
            return ss.str();
        } else {
            if (PofI && QofO) {
                ss<<"Strengthen Q so that Q(I,O) = false.";
            } else if (PofI && !QofO) {
                ss<<"Not corrections needed. ";
            } else if (!PofI && QofO) {
                ss<<"Weaken P so that P(I) = true, and strengthen Q so that Q(I,O) = false";
            } else if (!PofI && !QofO) {
                ss<<"Weaken P so that P(I) = true"<<endl;
            }
        }
    }
    return ss.str();
}

string
PDTCheckSpec :: recommendationString (
        PDTBehavior * beh, bool withCode,
        bool PofI, bool QofO,
        bool QofOPrime, bool oEqOPrime) {
    stringstream ss(stringstream::in | stringstream::out);

    ss << "Behavior: ";
    beh->toString(ss);
    ss << endl;

    if (withCode) {
        ss << "{P}S{Q}{B} Adequacy results: " << endl;
        ss << "  P(i):    " << PofI <<", ";
        ss << "Q(i,o):  " << QofO <<", ";
        ss << "Q(i,o'): " << QofOPrime<<",";
        ss << "o=o': " << oEqOPrime<<"." <<endl;

        if (beh->isGood()) {//good behaviors with code
            if (!PofI) {
                ss<<"Properties are not mature enough to test with code." << endl;
                return ss.str();
            }
            bool oInGofI = oEqOPrime;
            //TODO: if !oEqOPrime then prompt the user
            //      whether oPrime is in g(i)
            bool oInQofI = QofOPrime;
            ss << "Required: o in g(i) and Q(i,o)" <<endl;
            if (oInGofI && oInQofI) {
                ss << "Actual: o in g(i) and Q(i,o)" <<endl;
                ss << "Suggested Correction: " << endl;
                ss << "  No correction needed." << endl;
            }  else if (oInGofI && !oInQofI) {
                ss << "Actual: o in g(i) and (not Q(i,o))" <<endl;
                ss << "Suggested Correction: " << endl;
                ss << "  Weaken Q so that Q(i,o) = true." << endl;
            } else if (!oInGofI && oInQofI) {
                ss << "Actual: (o not in g(i)) and Q(i,o)" << endl;
                ss << "Suggested Correction: " << endl;
                ss << "  Strengthen Q so that Q(i,o) = true, and" << endl;
                ss << "  Strengthen S so that its output is in g(i)." << endl;
            } else {
                ss << "Actual: (o not in g(i)) and (not Q(i,o))" << endl;
                ss << "Suggested Correction: " << endl;
                ss << "  Strengthen S so that its output is in g(i)." << endl;
            }
        } else {// bad behaviors with code
            if (oEqOPrime) {
                ss<<"o is in g(i)"<<endl;
                if (QofOPrime) {
                    ss<<"o in VQ(i)"<<endl;
                    ss<<"Suggested Correction: "<<endl;
                    ss<<"  Strengthen Q so that Q(i,o) = false, and modify S so that o is not in S(i)"<<endl;
                } else {
                    ss<<"o is not in VQ(i)"<<endl;
                    ss<<"Suggested Correction: " << endl;
                    ss<<"  Modify S so that o is not in S(i)."<<endl;
                }
            } else {
                //TODO:
            }
        }
    }else {
        ss << "{P}-{Q}{B} adequacy results: " << endl;
        ss << "  P(i): " << PofI <<", Q(i,o): " << QofO <<". " << endl;

        if (beh->isGood() ) {
            if (PofI && QofO) {
                ss<<"Actual: P AND Q"<<endl;
                ss<<"Required: (NOT P) OR Q"<<endl;
                ss<<"Suggested Correction: choosing one of the following options:"<<endl;
                ss<<"  1. Strengthen P so that P(I) = false."<<endl;
                ss<<"  2. Skip."<<endl;
            } else if (PofI && !QofO) {
                ss<<"Actual: P AND (NOT Q)"<<endl;
                ss<<"Required: (NOT P) OR Q"<<endl;
                ss<<"Suggested Correction: choosing only one of the following options:"<<endl;
                ss<<"  1. Strengthen P so that P(I) = false."<<endl;
                ss<<"  2. Weaken Q so that Q(I,O) = true."<<endl;
            } else if (!PofI && QofO) {
                ss<<"Actual: (NOT P) AND Q"<<endl;
                ss<<"Required: (NOT P) OR Q"<<endl;
                ss<<"Suggested Correction: choosing only one of the following options:"<<endl;
                ss<<"  1. Weaken P so that P(I) = true."<<endl;
                ss<<"  2. Strengthen Q so that Q(I,O) = false."<<endl;
                ss<<"  3. Skip."<<endl;
            } else if (!PofI && !QofO) {
                ss<<"Actual: (NOT P) AND (NOT Q)"<<endl;
                ss<<"Required: (NOT P) OR Q"<<endl;
                ss<<"Suggested Correction: choosing one of the following options:"<<endl;
                ss<<"  1. Weaken P so that P(I) = true, and strengthen Q so that Q(I,O) = false."<<endl;
                ss<<"  2. Skip."<<endl;
            }
            return ss.str();
        } else {
            if (PofI && QofO) {
                ss<<"Actual: P AND Q"<<endl;
                ss<<"Required: P AND (NOT Q)"<<endl;
                ss<<"Suggested Correction: Strengthen Q so that Q(I,O) = false."<<endl;
            } else if (PofI && !QofO) {
                ss<<"Actual: P AND (NOT Q)"<<endl;
                ss<<"Required: P AND (NOT Q)"<<endl;
                ss<<"Not corrections needed. "<<endl;
            } else if (!PofI && QofO) {
                ss<<"Actual: (NOT P) AND Q"<<endl;
                ss<<"Required: P AND (NOT Q)"<<endl;
                ss<<"Suggested Correction: Weaken P so that P(I) = true, and strengthen Q so that Q(I,O) = false"<<endl;
            } else if (!PofI && !QofO) {
                ss<<"Actual: (NOT P) AND (NOT Q)"<<endl;
                ss<<"Required: P AND (NOT Q)"<<endl;
                ss<<"Suggested Correction: Weaken P so that P(I) = true"<<endl;
            }
        }
    }
    return ss.str();
}
